Inference at * 1 1 
Iof proof for Lemma p-mu-exists:



1. P : 
2. n : 
3. n1:. (n1 < n)  ((P(n1)))  (x: + Top. p-mu(P;x))
4. (P(n))
5. i:{0..n}. ((P(i)))
  x: + Top. p-mu(P;x) 

latex

 by ((ExRepD) 
CollapseTHEN (Using [`n1',i] (BHyp 3))) 
CollapseTHEN (Auto') 

latex

C.

Definitions

x:A. B(x), x:A  B(x), P  Q, x:A. B(x), x:AB(x), t  T, {i..j}, {x:A| B(x)}